Step of Proof: add_functionality_wrt_le 12,41

Inference at * 1 
Iof proof for Lemma add functionality wrt le:



1. i1 : 
2. i2 : 
3. j1 : 
4. j2 : 
5. i1  j1
6. i2  j2
  (i1+i2 (j1+j2
latex

 by MoveToConcl 3 
latex


 1

 1: 3. j2 : 
 1: 4. i2  j2
 1:   j1:. (i1  j1 ((i1+i2 (j1+j2))
 .


Definitionst  T, x:AB(x), P  Q

origin